da:fpf(Knd; k.Type), k:Knd. normal-da{i:l}(da)  normal-type{i:l}(ma-valtype(da; k)) 

latex

Definitions	normal-da{i:l}(da), ma-valtype(da; k), fpf-all(A; eq; f; x,v.P(x;v)), fpf-cap(f; eq; x; z), if b then t else f fi , fpf-ap(f; eq; x), left + right, Unit, P  Q, P  Q, x:A  B(x), fpf-dom(eq; x; f), Kind-deq, x:AB(x), fpf(A; a.B(a)), x. t(x), x.A(x), Type, Knd, prop{i:l}, s = t, , b, A, b, P  Q, t  T, x:A. B(x), normal-type{i:l}(T), top
Lemmas	normal-top, assert wf, not wf, bnot wf, bool wf, Knd wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf wf, fpf-ap wf, normal-type wf